(set-option :print-success false)
(set-logic QF_UFIDL)
; benchmark generated from python API
(set-info :status unknown)
(declare-fun c.sh_tl () Int)
(declare-fun qj1 () Int)
(declare-fun c.sh_hd () Int)
(declare-fun en_message () Int)
(declare-fun c.channel3 (Int) Int)
(declare-fun qi1 () Int)
(declare-fun c.sh_pos (Int) Int)
(declare-fun c.ArbVal (Int) Int)
(declare-fun c.ctr () Int)
(declare-fun c.home_current_client () Int)
(declare-fun c.channel2_4 (Int) Int)
(declare-fun en_cache_state () Int)
(declare-fun c.cache (Int) Int)
(declare-fun c.home_invalidate_list (Int) Bool)
(declare-fun c.home_exclusive_granted () Bool)
(declare-fun c.home_current_command () Int)
(declare-fun c.sh_q (Int) Int)
(declare-fun c.x3 () Bool)
(declare-fun c.x2 () Bool)
(declare-fun c.x1 () Bool)
(declare-fun c.x0 () Bool)

(push 2)
  (assert
   (let (($x40119 (< qj1 c.sh_tl)))
   (let (($x21952 (= c.sh_hd qj1)))
   (let (($x37693 (< c.sh_hd qj1)))
   (let (($x20865 (or $x37693 $x21952)))
   (let (($x361 (not $x20865)))
   (let (($x33696 (and $x361 $x40119)))
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x62427 (c.channel3 qi1)))
   (let (($x17495 (not (= ?x62427 ?x34831))))
   (and $x17495 $x33696))))))))))))))
  (assert
   (let ((?x71475 (c.ArbVal c.ctr)))
   (let ((?x9577 (c.sh_pos ?x71475)))
   (let (($x7942 (< ?x9577 c.sh_tl)))
   (let (($x2377 (not $x7942)))
   (let (($x41171 (= c.sh_hd ?x9577)))
   (let (($x77764 (< c.sh_hd ?x9577)))
   (let (($x36355 (or $x77764 $x41171)))
   (let (($x39464 (and $x36355 $x2377)))
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x28955 (c.channel3 c.home_current_client)))
   (let (($x81758 (not (= ?x28955 ?x34831))))
   (let (($x6084 (and $x81758 $x39464)))
   (let (($x63275 (not (= (c.channel2_4 c.home_current_client) ?x30209))))
   (let (($x28518 (and $x63275 $x6084)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x60908 (+ 1 ?x34647)))
   (let ((?x30972 (c.channel2_4 c.home_current_client)))
   (let (($x50264 (= ?x30972 ?x60908)))
   (let (($x12721 (not $x50264)))
   (let (($x65324 (and $x12721 $x28518)))
   (let (($x31844 (= ?x30972 ?x34647)))
   (let (($x22853 (and $x31844 $x65324)))
   (let ((?x32741 (c.cache c.home_current_client)))
   (let (($x71752 (= ?x32741 en_cache_state)))
   (let (($x58513 (and $x71752 $x22853)))
   (let (($x64615 (not (= ?x32741 (+ 1 (+ 1 en_cache_state))))))
   (let (($x22973 (and $x64615 $x58513)))
   (let (($x32504 (not (c.home_invalidate_list c.home_current_client))))
   (let (($x33535 (and $x32504 $x22973)))
   (let (($x62406 (= c.sh_hd c.sh_tl)))
   (let (($x27620 (not $x62406)))
   (let (($x32228 (and $x27620 $x33535)))
   (let (($x9751 (not c.home_exclusive_granted)))
   (let (($x82467 (and $x9751 $x32228)))
   (let (($x19312 (= c.home_current_command ?x1486)))
   (let (($x44417 (not $x19312)))
   (let (($x82464 (and $x44417 $x82467)))
   (let (($x37805 (= c.home_current_command ?x46960)))
   (let (($x30892 (not $x37805)))
   (let (($x82487 (and $x30892 $x82464)))
   (let ((?x23348 (c.sh_q c.sh_hd)))
   (let (($x57487 (= c.home_current_client ?x23348)))
   (let (($x82488 (and $x57487 $x82487)))
   (not $x82488))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(pop 0)

(push 2)
  (assert
   (let ((?x7929 (c.sh_pos qi1)))
   (= c.sh_hd ?x7929)))
  (assert
   (let ((?x12727 (c.sh_pos c.home_current_client)))
   (let (($x77351 (< ?x12727 c.sh_tl)))
   (let (($x77120 (= c.sh_hd ?x12727)))
   (let (($x47506 (< c.sh_hd ?x12727)))
   (let (($x30131 (or $x47506 $x77120)))
   (let (($x67392 (not $x30131)))
   (let (($x42448 (and $x67392 $x77351)))
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x62427 (c.channel3 qi1)))
   (let (($x17495 (not (= ?x62427 ?x34831))))
   (let (($x62725 (and $x17495 $x42448)))
   (let (($x12114 (not (= (c.channel2_4 qi1) ?x30209))))
   (let (($x55079 (and $x12114 $x62725)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x60908 (+ 1 ?x34647)))
   (let ((?x83998 (c.channel2_4 qi1)))
   (let (($x63890 (= ?x83998 ?x60908)))
   (let (($x10956 (not $x63890)))
   (let (($x55332 (and $x10956 $x55079)))
   (let (($x63682 (= ?x83998 ?x34647)))
   (let (($x16799 (not $x63682)))
   (let (($x56754 (and $x16799 $x55332)))
   (let ((?x46718 (c.cache qi1)))
   (let (($x83356 (= ?x46718 en_cache_state)))
   (let (($x57544 (and $x83356 $x56754)))
   (let (($x8143 (not (= ?x46718 (+ 1 (+ 1 en_cache_state))))))
   (let (($x26835 (and $x8143 $x57544)))
   (let (($x7005 (c.home_invalidate_list qi1)))
   (let (($x41153 (not $x7005)))
   (let (($x83211 (and $x41153 $x26835)))
   (let (($x62406 (= c.sh_hd c.sh_tl)))
   (let (($x27620 (not $x62406)))
   (let (($x72571 (and $x27620 $x83211)))
   (let (($x19312 (= c.home_current_command ?x1486)))
   (let (($x44417 (not $x19312)))
   (let (($x73799 (and $x44417 $x72571)))
   (let (($x37805 (= c.home_current_command ?x46960)))
   (let (($x30892 (not $x37805)))
   (let (($x51797 (and $x30892 $x73799)))
   (not $x51797))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(pop 0)

(push 2)
  (assert
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x62427 (c.channel3 qi1)))
   (let (($x17495 (not (= ?x62427 ?x34831))))
   (let (($x12114 (not (= (c.channel2_4 qi1) ?x30209))))
   (let (($x24980 (and $x12114 $x17495)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x60908 (+ 1 ?x34647)))
   (let ((?x83998 (c.channel2_4 qi1)))
   (let (($x63890 (= ?x83998 ?x60908)))
   (let (($x10956 (not $x63890)))
   (let (($x80738 (and $x10956 $x24980)))
   (let (($x63682 (= ?x83998 ?x34647)))
   (let (($x16799 (not $x63682)))
   (let (($x59652 (and $x16799 $x80738)))
   (let ((?x46718 (c.cache qi1)))
   (let (($x83356 (= ?x46718 en_cache_state)))
   (let (($x64250 (and $x83356 $x59652)))
   (let (($x8143 (not (= ?x46718 (+ 1 (+ 1 en_cache_state))))))
   (let (($x72118 (and $x8143 $x64250)))
   (let (($x7005 (c.home_invalidate_list qi1)))
   (let (($x41153 (not $x7005)))
   (let (($x34348 (and $x41153 $x72118)))
   (not $x34348)))))))))))))))))))))))))))
  (assert
   (let ((?x71475 (c.ArbVal c.ctr)))
   (let ((?x9577 (c.sh_pos ?x71475)))
   (let (($x7942 (< ?x9577 c.sh_tl)))
   (let (($x41171 (= c.sh_hd ?x9577)))
   (let (($x77764 (< c.sh_hd ?x9577)))
   (let (($x36355 (or $x77764 $x41171)))
   (let (($x54592 (not $x36355)))
   (let (($x5247 (and $x54592 $x7942)))
   (not $x5247))))))))))
(check-sat)
(pop 2)

(push 2)
  (assert
   (let ((?x12727 (c.sh_pos c.home_current_client)))
   (let (($x77351 (< ?x12727 c.sh_tl)))
   (let (($x77120 (= c.sh_hd ?x12727)))
   (let (($x47506 (< c.sh_hd ?x12727)))
   (let (($x30131 (or $x47506 $x77120)))
   (let (($x67392 (not $x30131)))
   (let (($x42448 (and $x67392 $x77351)))
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x28955 (c.channel3 c.home_current_client)))
   (let (($x81758 (not (= ?x28955 ?x34831))))
   (let (($x22606 (and $x81758 $x42448)))
   (let (($x63275 (not (= (c.channel2_4 c.home_current_client) ?x30209))))
   (let (($x11172 (and $x63275 $x22606)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x60908 (+ 1 ?x34647)))
   (let ((?x30972 (c.channel2_4 c.home_current_client)))
   (let (($x50264 (= ?x30972 ?x60908)))
   (let (($x12721 (not $x50264)))
   (let (($x3408 (and $x12721 $x11172)))
   (let (($x31844 (= ?x30972 ?x34647)))
   (let (($x33315 (not $x31844)))
   (let (($x34421 (and $x33315 $x3408)))
   (let ((?x32741 (c.cache c.home_current_client)))
   (let (($x71752 (= ?x32741 en_cache_state)))
   (let (($x77467 (and $x71752 $x34421)))
   (let (($x64615 (not (= ?x32741 (+ 1 (+ 1 en_cache_state))))))
   (let (($x34996 (and $x64615 $x77467)))
   (let (($x32504 (not (c.home_invalidate_list c.home_current_client))))
   (let (($x83118 (and $x32504 $x34996)))
   (let (($x62406 (= c.sh_hd c.sh_tl)))
   (let (($x27620 (not $x62406)))
   (let (($x79986 (and $x27620 $x83118)))
   (let (($x19312 (= c.home_current_command ?x1486)))
   (let (($x44417 (not $x19312)))
   (let (($x7254 (and $x44417 $x79986)))
   (let (($x37805 (= c.home_current_command ?x46960)))
   (let (($x30892 (not $x37805)))
   (let (($x55329 (and $x30892 $x7254)))
   (let ((?x23348 (c.sh_q c.sh_hd)))
   (let (($x57487 (= c.home_current_client ?x23348)))
   (let (($x81471 (not $x57487)))
   (let (($x20266 (and $x81471 $x55329)))
   (not $x20266)))))))))))))))))))))))))))))))))))))))))))))))
  (assert
   (let ((?x71475 (c.ArbVal c.ctr)))
   (let ((?x9577 (c.sh_pos ?x71475)))
   (let (($x7942 (< ?x9577 c.sh_tl)))
   (let (($x41171 (= c.sh_hd ?x9577)))
   (let (($x77764 (< c.sh_hd ?x9577)))
   (let (($x36355 (or $x77764 $x41171)))
   (let (($x54592 (not $x36355)))
   (let (($x5247 (and $x54592 $x7942)))
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x28955 (c.channel3 c.home_current_client)))
   (let (($x81758 (not (= ?x28955 ?x34831))))
   (let (($x38444 (and $x81758 $x5247)))
   (let (($x63275 (not (= (c.channel2_4 c.home_current_client) ?x30209))))
   (let (($x54630 (and $x63275 $x38444)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x60908 (+ 1 ?x34647)))
   (let ((?x30972 (c.channel2_4 c.home_current_client)))
   (let (($x50264 (= ?x30972 ?x60908)))
   (let (($x12721 (not $x50264)))
   (let (($x69808 (and $x12721 $x54630)))
   (let (($x31844 (= ?x30972 ?x34647)))
   (let (($x70967 (and $x31844 $x69808)))
   (let ((?x32741 (c.cache c.home_current_client)))
   (let (($x71752 (= ?x32741 en_cache_state)))
   (let (($x47288 (and $x71752 $x70967)))
   (let (($x64615 (not (= ?x32741 (+ 1 (+ 1 en_cache_state))))))
   (let (($x47537 (and $x64615 $x47288)))
   (let (($x32504 (not (c.home_invalidate_list c.home_current_client))))
   (let (($x33335 (and $x32504 $x47537)))
   (let (($x62406 (= c.sh_hd c.sh_tl)))
   (let (($x27620 (not $x62406)))
   (let (($x78532 (and $x27620 $x33335)))
   (let (($x9751 (not c.home_exclusive_granted)))
   (let (($x12969 (and $x9751 $x78532)))
   (let (($x19312 (= c.home_current_command ?x1486)))
   (let (($x44417 (not $x19312)))
   (let (($x47762 (and $x44417 $x12969)))
   (let (($x37805 (= c.home_current_command ?x46960)))
   (let (($x30892 (not $x37805)))
   (let (($x22841 (and $x30892 $x47762)))
   (let ((?x23348 (c.sh_q c.sh_hd)))
   (let (($x57487 (= c.home_current_client ?x23348)))
   (let (($x4066 (and $x57487 $x22841)))
   (let ((?x12727 (c.sh_pos c.home_current_client)))
   (let (($x30901 (= ?x12727 ?x9577)))
   (let (($x77440 (not $x30901)))
   (let (($x46807 (and $x77440 $x4066)))
   (let (($x82455 (and $x50264 $x54630)))
   (let (($x33315 (not $x31844)))
   (let (($x82456 (and $x33315 $x82455)))
   (let (($x44096 (and $x71752 $x82456)))
   (let (($x22719 (and $x64615 $x44096)))
   (let (($x33065 (and $x32504 $x22719)))
   (let (($x22836 (and $x27620 $x33065)))
   (let (($x47499 (and c.home_exclusive_granted $x22836)))
   (let (($x46898 (and $x44417 $x47499)))
   (let (($x26248 (and $x30892 $x46898)))
   (let (($x46918 (and $x57487 $x26248)))
   (let (($x76121 (and $x77440 $x46918)))
   (let (($x78645 (and $x81758 $x36355)))
   (let (($x46460 (and $x63275 $x78645)))
   (let (($x46717 (and $x12721 $x46460)))
   (let (($x70234 (and $x33315 $x46717)))
   (let (($x69439 (and $x71752 $x70234)))
   (let (($x32094 (and $x64615 $x69439)))
   (let (($x83845 (and $x32504 $x32094)))
   (let (($x26645 (and $x27620 $x83845)))
   (let (($x22620 (and $x44417 $x26645)))
   (let (($x81024 (and $x30892 $x22620)))
   (let (($x81471 (not $x57487)))
   (let (($x74542 (and $x81471 $x81024)))
   (let ((?x3281 (c.sh_q ?x9577)))
   (let (($x35377 (= c.home_current_client ?x3281)))
   (let (($x46398 (not $x35377)))
   (let (($x82505 (and $x46398 $x74542)))
   (let (($x2377 (not $x7942)))
   (let (($x39464 (and $x36355 $x2377)))
   (let (($x6084 (and $x81758 $x39464)))
   (let (($x28518 (and $x63275 $x6084)))
   (let (($x65324 (and $x12721 $x28518)))
   (let (($x38508 (and $x33315 $x65324)))
   (let (($x38295 (and $x71752 $x38508)))
   (let (($x38294 (and $x64615 $x38295)))
   (let (($x52324 (and $x32504 $x38294)))
   (let (($x46509 (and $x27620 $x52324)))
   (let (($x46281 (and $x44417 $x46509)))
   (let (($x79825 (and $x30892 $x46281)))
   (let (($x46291 (and $x81471 $x79825)))
   (let (($x35011 (and $x62406 $x52324)))
   (let (($x36770 (and $x9751 $x35011)))
   (let (($x63399 (and $x30892 $x36770)))
   (let (($x38532 (and $x33315 $x69808)))
   (let (($x25006 (and $x71752 $x38532)))
   (let (($x38589 (and $x64615 $x25006)))
   (let (($x45399 (and $x32504 $x38589)))
   (let (($x80682 (and $x27620 $x45399)))
   (let (($x40599 (and $x44417 $x80682)))
   (let (($x80887 (and $x30892 $x40599)))
   (let (($x79146 (and $x81471 $x80887)))
   (let (($x77974 (and $x62406 $x45399)))
   (let (($x63911 (and $x9751 $x77974)))
   (let (($x80502 (and $x30892 $x63911)))
   (let (($x40817 (and $x44417 $x36770)))
   (let (($x77295 (and $x44417 $x63911)))
   (let (($x26710 (or $x77295 $x40817)))
   (let (($x33974 (or $x26710 $x80502)))
   (let (($x21396 (or $x33974 $x79146)))
   (let (($x21417 (or $x21396 $x63399)))
   (let (($x59676 (or $x21417 $x46291)))
   (let (($x82454 (or $x59676 $x82505)))
   (let (($x47192 (or $x82454 $x76121)))
   (let (($x31553 (or $x47192 $x46807)))
   (not $x31553)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(pop 2)

(push 2)
  (assert
   (let ((?x1486 (+ 1 en_message)))
   (let (($x19312 (= c.home_current_command ?x1486)))
   (let (($x44417 (not $x19312)))
   (let ((?x12727 (c.sh_pos c.home_current_client)))
   (let (($x77351 (< ?x12727 c.sh_tl)))
   (let (($x77120 (= c.sh_hd ?x12727)))
   (let (($x47506 (< c.sh_hd ?x12727)))
   (let (($x30131 (or $x47506 $x77120)))
   (let (($x67392 (not $x30131)))
   (let (($x42448 (and $x67392 $x77351)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x28955 (c.channel3 c.home_current_client)))
   (let (($x81758 (not (= ?x28955 ?x34831))))
   (let (($x22606 (and $x81758 $x42448)))
   (let (($x63275 (not (= (c.channel2_4 c.home_current_client) ?x30209))))
   (let (($x11172 (and $x63275 $x22606)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x60908 (+ 1 ?x34647)))
   (let ((?x30972 (c.channel2_4 c.home_current_client)))
   (let (($x50264 (= ?x30972 ?x60908)))
   (let (($x12721 (not $x50264)))
   (let (($x3408 (and $x12721 $x11172)))
   (let (($x31844 (= ?x30972 ?x34647)))
   (let (($x33315 (not $x31844)))
   (let (($x34421 (and $x33315 $x3408)))
   (let ((?x32741 (c.cache c.home_current_client)))
   (let (($x71752 (= ?x32741 en_cache_state)))
   (let (($x77467 (and $x71752 $x34421)))
   (let (($x36396 (and $x77467 $x44417)))
   (not $x36396)))))))))))))))))))))))))))))))))
  (assert
   (let (($x40119 (< qj1 c.sh_tl)))
   (let (($x21952 (= c.sh_hd qj1)))
   (let (($x37693 (< c.sh_hd qj1)))
   (let (($x20865 (or $x37693 $x21952)))
   (let (($x361 (not $x20865)))
   (let (($x33696 (and $x361 $x40119)))
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x62427 (c.channel3 qi1)))
   (let (($x17495 (not (= ?x62427 ?x34831))))
   (let (($x36851 (and $x17495 $x33696)))
   (let (($x12114 (not (= (c.channel2_4 qi1) ?x30209))))
   (let (($x40627 (and $x12114 $x36851)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x60908 (+ 1 ?x34647)))
   (let ((?x83998 (c.channel2_4 qi1)))
   (let (($x63890 (= ?x83998 ?x60908)))
   (let (($x10956 (not $x63890)))
   (let (($x22295 (and $x10956 $x40627)))
   (let ((?x75590 (+ 1 c.sh_hd)))
   (let (($x30269 (< ?x75590 c.sh_tl)))
   (let (($x59696 (not $x30269)))
   (let (($x49587 (and $x17495 $x59696)))
   (let (($x75364 (and $x12114 $x49587)))
   (let (($x51249 (and $x63890 $x75364)))
   (let (($x63682 (= ?x83998 ?x34647)))
   (let (($x16799 (not $x63682)))
   (let (($x64373 (and $x16799 $x51249)))
   (let ((?x46718 (c.cache qi1)))
   (let (($x83356 (= ?x46718 en_cache_state)))
   (let (($x24821 (and $x83356 $x64373)))
   (let (($x8143 (not (= ?x46718 (+ 1 (+ 1 en_cache_state))))))
   (let (($x24801 (and $x8143 $x24821)))
   (let (($x7005 (c.home_invalidate_list qi1)))
   (let (($x41153 (not $x7005)))
   (let (($x52058 (and $x41153 $x24801)))
   (let (($x62406 (= c.sh_hd c.sh_tl)))
   (let (($x27620 (not $x62406)))
   (let (($x52761 (and $x27620 $x52058)))
   (let (($x13288 (not (= (c.cache (c.ArbVal c.ctr)) (+ 1 (+ 1 en_cache_state))))))
   (let (($x49848 (and $x13288 $x52761)))
   (let (($x60965 (and $x49848 $x22295)))
   (not $x60965))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(pop 2)

(push 2)
  (assert
   (let ((?x12727 (c.sh_pos c.home_current_client)))
   (let (($x77351 (< ?x12727 c.sh_tl)))
   (let (($x20992 (not $x77351)))
   (let (($x77120 (= c.sh_hd ?x12727)))
   (let (($x47506 (< c.sh_hd ?x12727)))
   (let (($x30131 (or $x47506 $x77120)))
   (let (($x11057 (and $x30131 $x20992)))
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x71475 (c.ArbVal c.ctr)))
   (let ((?x58566 (c.channel3 ?x71475)))
   (let (($x49145 (= ?x58566 ?x34831)))
   (let (($x33193 (not $x49145)))
   (let (($x73356 (and $x33193 $x11057)))
   (let ((?x13783 (c.channel2_4 ?x71475)))
   (let (($x16165 (= ?x13783 ?x30209)))
   (let (($x14680 (not $x16165)))
   (let (($x65513 (and $x14680 $x73356)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x60908 (+ 1 ?x34647)))
   (let (($x2646 (= ?x13783 ?x60908)))
   (let (($x1508 (not $x2646)))
   (let (($x7626 (and $x1508 $x65513)))
   (let (($x13844 (= ?x13783 ?x34647)))
   (let (($x25985 (not $x13844)))
   (let (($x8596 (and $x25985 $x7626)))
   (let ((?x12944 (c.cache ?x71475)))
   (let (($x13259 (= ?x12944 en_cache_state)))
   (let (($x26692 (and $x13259 $x8596)))
   (let (($x13288 (not (= ?x12944 (+ 1 (+ 1 en_cache_state))))))
   (let (($x46106 (and $x13288 $x26692)))
   (let (($x74119 (c.home_invalidate_list ?x71475)))
   (let (($x77139 (not $x74119)))
   (let (($x6364 (and $x77139 $x46106)))
   (let (($x62406 (= c.sh_hd c.sh_tl)))
   (let (($x21470 (and $x62406 $x6364)))
   (let (($x9751 (not c.home_exclusive_granted)))
   (let (($x41897 (and $x9751 $x21470)))
   (not $x41897))))))))))))))))))))))))))))))))))))))))))
  (assert
   (let ((?x71475 (c.ArbVal c.ctr)))
   (let ((?x9577 (c.sh_pos ?x71475)))
   (let (($x41171 (= c.sh_hd ?x9577)))
   (let (($x77764 (< c.sh_hd ?x9577)))
   (let (($x36355 (or $x77764 $x41171)))
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x28955 (c.channel3 c.home_current_client)))
   (let (($x81758 (not (= ?x28955 ?x34831))))
   (let (($x78645 (and $x81758 $x36355)))
   (let (($x63275 (not (= (c.channel2_4 c.home_current_client) ?x30209))))
   (let (($x46460 (and $x63275 $x78645)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x60908 (+ 1 ?x34647)))
   (let ((?x30972 (c.channel2_4 c.home_current_client)))
   (let (($x50264 (= ?x30972 ?x60908)))
   (let (($x12721 (not $x50264)))
   (let (($x46717 (and $x12721 $x46460)))
   (let (($x31844 (= ?x30972 ?x34647)))
   (let (($x33315 (not $x31844)))
   (let (($x70234 (and $x33315 $x46717)))
   (let ((?x32741 (c.cache c.home_current_client)))
   (let (($x71752 (= ?x32741 en_cache_state)))
   (let (($x69439 (and $x71752 $x70234)))
   (let (($x64615 (not (= ?x32741 (+ 1 (+ 1 en_cache_state))))))
   (let (($x32094 (and $x64615 $x69439)))
   (let (($x32504 (not (c.home_invalidate_list c.home_current_client))))
   (let (($x83845 (and $x32504 $x32094)))
   (let (($x62406 (= c.sh_hd c.sh_tl)))
   (let (($x27620 (not $x62406)))
   (let (($x26645 (and $x27620 $x83845)))
   (let (($x19312 (= c.home_current_command ?x1486)))
   (let (($x44417 (not $x19312)))
   (let (($x22620 (and $x44417 $x26645)))
   (let (($x37805 (= c.home_current_command ?x46960)))
   (let (($x30892 (not $x37805)))
   (let (($x81024 (and $x30892 $x22620)))
   (let ((?x23348 (c.sh_q c.sh_hd)))
   (let (($x57487 (= c.home_current_client ?x23348)))
   (let (($x81471 (not $x57487)))
   (let (($x74542 (and $x81471 $x81024)))
   (let ((?x3281 (c.sh_q ?x9577)))
   (let (($x35377 (= c.home_current_client ?x3281)))
   (let (($x46398 (not $x35377)))
   (let (($x82505 (and $x46398 $x74542)))
   (let (($x7942 (< ?x9577 c.sh_tl)))
   (let (($x2377 (not $x7942)))
   (let (($x39464 (and $x36355 $x2377)))
   (let (($x6084 (and $x81758 $x39464)))
   (let (($x28518 (and $x63275 $x6084)))
   (let (($x65324 (and $x12721 $x28518)))
   (let (($x38508 (and $x33315 $x65324)))
   (let (($x38295 (and $x71752 $x38508)))
   (let (($x38294 (and $x64615 $x38295)))
   (let (($x52324 (and $x32504 $x38294)))
   (let (($x46509 (and $x27620 $x52324)))
   (let (($x46281 (and $x44417 $x46509)))
   (let (($x79825 (and $x30892 $x46281)))
   (let (($x46291 (and $x81471 $x79825)))
   (let (($x35011 (and $x62406 $x52324)))
   (let (($x9751 (not c.home_exclusive_granted)))
   (let (($x36770 (and $x9751 $x35011)))
   (let (($x63399 (and $x30892 $x36770)))
   (let (($x54592 (not $x36355)))
   (let (($x5247 (and $x54592 $x7942)))
   (let (($x38444 (and $x81758 $x5247)))
   (let (($x54630 (and $x63275 $x38444)))
   (let (($x69808 (and $x12721 $x54630)))
   (let (($x38532 (and $x33315 $x69808)))
   (let (($x25006 (and $x71752 $x38532)))
   (let (($x38589 (and $x64615 $x25006)))
   (let (($x45399 (and $x32504 $x38589)))
   (let (($x80682 (and $x27620 $x45399)))
   (let (($x40599 (and $x44417 $x80682)))
   (let (($x80887 (and $x30892 $x40599)))
   (let (($x79146 (and $x81471 $x80887)))
   (let (($x77974 (and $x62406 $x45399)))
   (let (($x63911 (and $x9751 $x77974)))
   (let (($x80502 (and $x30892 $x63911)))
   (let (($x40817 (and $x44417 $x36770)))
   (let (($x77295 (and $x44417 $x63911)))
   (let (($x26710 (or $x77295 $x40817)))
   (let (($x33974 (or $x26710 $x80502)))
   (let (($x21396 (or $x33974 $x79146)))
   (let (($x21417 (or $x21396 $x63399)))
   (let (($x59676 (or $x21417 $x46291)))
   (let (($x82454 (or $x59676 $x82505)))
   (not $x82454)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(pop 2)

(push 2)
  (assert
   (let ((?x75590 (+ 1 c.sh_hd)))
   (let (($x30269 (< ?x75590 c.sh_tl)))
   (let (($x59696 (not $x30269)))
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x28955 (c.channel3 c.home_current_client)))
   (let (($x81758 (not (= ?x28955 ?x34831))))
   (let (($x43674 (and $x81758 $x59696)))
   (let (($x63275 (not (= (c.channel2_4 c.home_current_client) ?x30209))))
   (let (($x39497 (and $x63275 $x43674)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x60908 (+ 1 ?x34647)))
   (let ((?x30972 (c.channel2_4 c.home_current_client)))
   (let (($x50264 (= ?x30972 ?x60908)))
   (let (($x12721 (not $x50264)))
   (let (($x31461 (and $x12721 $x39497)))
   (let (($x31844 (= ?x30972 ?x34647)))
   (let (($x33315 (not $x31844)))
   (let (($x38626 (and $x33315 $x31461)))
   (not $x38626)))))))))))))))))))))))
  (assert
   (let ((?x71475 (c.ArbVal c.ctr)))
   (let ((?x9577 (c.sh_pos ?x71475)))
   (let (($x7942 (< ?x9577 c.sh_tl)))
   (let (($x2377 (not $x7942)))
   (let (($x41171 (= c.sh_hd ?x9577)))
   (let (($x77764 (< c.sh_hd ?x9577)))
   (let (($x36355 (or $x77764 $x41171)))
   (let (($x39464 (and $x36355 $x2377)))
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x28955 (c.channel3 c.home_current_client)))
   (let (($x81758 (not (= ?x28955 ?x34831))))
   (let (($x6084 (and $x81758 $x39464)))
   (let (($x63275 (not (= (c.channel2_4 c.home_current_client) ?x30209))))
   (let (($x28518 (and $x63275 $x6084)))
   (let (($x11602 (not $x28518)))
   (not $x11602))))))))))))))))))))
(check-sat)
(pop 1)

(push 2)
  (assert
   (let ((?x32741 (c.cache c.home_current_client)))
   (let (($x71752 (= ?x32741 en_cache_state)))
   (let (($x50650 (not $x71752)))
   (not $x50650)))))
  (assert
   (let (($x62406 (= c.sh_hd c.sh_tl)))
   (let (($x27620 (not $x62406)))
   (let (($x61117 (not $x27620)))
   (not $x61117)))))
(check-sat)
(pop 2)

(push 2)
  (assert
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x30972 (c.channel2_4 c.home_current_client)))
   (let (($x31844 (= ?x30972 ?x34647)))
   (let (($x33315 (not $x31844)))
   (let ((?x12727 (c.sh_pos c.home_current_client)))
   (let (($x77351 (< ?x12727 c.sh_tl)))
   (let (($x77120 (= c.sh_hd ?x12727)))
   (let (($x47506 (< c.sh_hd ?x12727)))
   (let (($x30131 (or $x47506 $x77120)))
   (let (($x67392 (not $x30131)))
   (let (($x42448 (and $x67392 $x77351)))
   (let (($x81758 (not (= (c.channel3 c.home_current_client) ?x34831))))
   (let (($x22606 (and $x81758 $x42448)))
   (let (($x63275 (not (= ?x30972 ?x30209))))
   (let (($x11172 (and $x63275 $x22606)))
   (let ((?x60908 (+ 1 ?x34647)))
   (let (($x50264 (= ?x30972 ?x60908)))
   (let (($x12721 (not $x50264)))
   (let (($x3408 (and $x12721 $x11172)))
   (let (($x34421 (and $x33315 $x3408)))
   (let ((?x32741 (c.cache c.home_current_client)))
   (let (($x71752 (= ?x32741 en_cache_state)))
   (let (($x77467 (and $x71752 $x34421)))
   (let (($x64615 (not (= ?x32741 (+ 1 (+ 1 en_cache_state))))))
   (let (($x34996 (and $x64615 $x77467)))
   (let (($x32504 (not (c.home_invalidate_list c.home_current_client))))
   (let (($x83118 (and $x32504 $x34996)))
   (let (($x62406 (= c.sh_hd c.sh_tl)))
   (let (($x37554 (and $x62406 $x83118)))
   (let (($x9751 (not c.home_exclusive_granted)))
   (let (($x579 (and $x9751 $x37554)))
   (let (($x18159 (and $x579 $x33315)))
   (not $x18159))))))))))))))))))))))))))))))))))))))
  (assert
   (let ((?x71475 (c.ArbVal c.ctr)))
   (let ((?x9577 (c.sh_pos ?x71475)))
   (let (($x7942 (< ?x9577 c.sh_tl)))
   (let (($x41171 (= c.sh_hd ?x9577)))
   (let (($x77764 (< c.sh_hd ?x9577)))
   (let (($x36355 (or $x77764 $x41171)))
   (let (($x54592 (not $x36355)))
   (let (($x5247 (and $x54592 $x7942)))
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x62427 (c.channel3 qi1)))
   (let (($x17495 (not (= ?x62427 ?x34831))))
   (let (($x70583 (and $x17495 $x5247)))
   (let (($x12114 (not (= (c.channel2_4 qi1) ?x30209))))
   (let (($x63851 (and $x12114 $x70583)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x60908 (+ 1 ?x34647)))
   (let ((?x83998 (c.channel2_4 qi1)))
   (let (($x63890 (= ?x83998 ?x60908)))
   (let (($x10956 (not $x63890)))
   (let (($x8032 (and $x10956 $x63851)))
   (let (($x63682 (= ?x83998 ?x34647)))
   (let (($x16799 (not $x63682)))
   (let (($x8202 (and $x16799 $x8032)))
   (let ((?x46718 (c.cache qi1)))
   (let (($x83356 (= ?x46718 en_cache_state)))
   (let (($x3155 (and $x83356 $x8202)))
   (let (($x8143 (not (= ?x46718 (+ 1 (+ 1 en_cache_state))))))
   (let (($x43398 (and $x8143 $x3155)))
   (let (($x7005 (c.home_invalidate_list qi1)))
   (let (($x41153 (not $x7005)))
   (let (($x2005 (and $x41153 $x43398)))
   (let (($x62406 (= c.sh_hd c.sh_tl)))
   (let (($x27620 (not $x62406)))
   (let (($x2034 (and $x27620 $x2005)))
   (not $x2034)))))))))))))))))))))))))))))))))))))))
(check-sat)
(pop 1)

(push 2)
  (assert
   (let ((?x71475 (c.ArbVal c.ctr)))
   (let ((?x9577 (c.sh_pos ?x71475)))
   (let (($x7942 (< ?x9577 c.sh_tl)))
   (let (($x2377 (not $x7942)))
   (let (($x41171 (= c.sh_hd ?x9577)))
   (let (($x77764 (< c.sh_hd ?x9577)))
   (let (($x36355 (or $x77764 $x41171)))
   (let (($x39464 (and $x36355 $x2377)))
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x28955 (c.channel3 c.home_current_client)))
   (let (($x81758 (not (= ?x28955 ?x34831))))
   (let (($x6084 (and $x81758 $x39464)))
   (let (($x63275 (not (= (c.channel2_4 c.home_current_client) ?x30209))))
   (let (($x28518 (and $x63275 $x6084)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x60908 (+ 1 ?x34647)))
   (let ((?x30972 (c.channel2_4 c.home_current_client)))
   (let (($x50264 (= ?x30972 ?x60908)))
   (let (($x12721 (not $x50264)))
   (let (($x65324 (and $x12721 $x28518)))
   (let (($x31844 (= ?x30972 ?x34647)))
   (let (($x22853 (and $x31844 $x65324)))
   (let ((?x32741 (c.cache c.home_current_client)))
   (let (($x71752 (= ?x32741 en_cache_state)))
   (let (($x58513 (and $x71752 $x22853)))
   (let (($x64615 (not (= ?x32741 (+ 1 (+ 1 en_cache_state))))))
   (let (($x22973 (and $x64615 $x58513)))
   (let (($x32504 (not (c.home_invalidate_list c.home_current_client))))
   (let (($x33535 (and $x32504 $x22973)))
   (let (($x62406 (= c.sh_hd c.sh_tl)))
   (let (($x27620 (not $x62406)))
   (let (($x32228 (and $x27620 $x33535)))
   (let (($x9751 (not c.home_exclusive_granted)))
   (let (($x82467 (and $x9751 $x32228)))
   (let (($x19312 (= c.home_current_command ?x1486)))
   (let (($x44417 (not $x19312)))
   (let (($x82464 (and $x44417 $x82467)))
   (let (($x37805 (= c.home_current_command ?x46960)))
   (let (($x30892 (not $x37805)))
   (let (($x82487 (and $x30892 $x82464)))
   (let ((?x23348 (c.sh_q c.sh_hd)))
   (let (($x57487 (= c.home_current_client ?x23348)))
   (let (($x82488 (and $x57487 $x82487)))
   (not $x82488))))))))))))))))))))))))))))))))))))))))))))))))
  (assert
   (< qj1 c.sh_tl))
(check-sat)
(pop 0)

(push 2)
  (assert
   (let (($x40119 (< qj1 c.sh_tl)))
   (let (($x21952 (= c.sh_hd qj1)))
   (let (($x37693 (< c.sh_hd qj1)))
   (let (($x20865 (or $x37693 $x21952)))
   (let (($x4661 (and $x20865 $x40119)))
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x62427 (c.channel3 qi1)))
   (let (($x17495 (not (= ?x62427 ?x34831))))
   (let (($x13915 (and $x17495 $x4661)))
   (let (($x12114 (not (= (c.channel2_4 qi1) ?x30209))))
   (let (($x2706 (and $x12114 $x13915)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x60908 (+ 1 ?x34647)))
   (let ((?x83998 (c.channel2_4 qi1)))
   (let (($x63890 (= ?x83998 ?x60908)))
   (let (($x10956 (not $x63890)))
   (let (($x43764 (and $x10956 $x2706)))
   (let (($x63682 (= ?x83998 ?x34647)))
   (let (($x34802 (and $x63682 $x43764)))
   (let ((?x46718 (c.cache qi1)))
   (let (($x83356 (= ?x46718 en_cache_state)))
   (let (($x56613 (and $x83356 $x34802)))
   (let (($x8143 (not (= ?x46718 (+ 1 (+ 1 en_cache_state))))))
   (let (($x32928 (and $x8143 $x56613)))
   (let (($x7005 (c.home_invalidate_list qi1)))
   (let (($x41153 (not $x7005)))
   (let (($x130 (and $x41153 $x32928)))
   (let (($x62406 (= c.sh_hd c.sh_tl)))
   (let (($x27620 (not $x62406)))
   (let (($x33613 (and $x27620 $x130)))
   (not $x33613)))))))))))))))))))))))))))))))))))
  (assert
   (let ((?x12727 (c.sh_pos c.home_current_client)))
   (let (($x77351 (< ?x12727 c.sh_tl)))
   (let (($x20992 (not $x77351)))
   (let (($x77120 (= c.sh_hd ?x12727)))
   (let (($x47506 (< c.sh_hd ?x12727)))
   (let (($x30131 (or $x47506 $x77120)))
   (let (($x11057 (and $x30131 $x20992)))
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x71475 (c.ArbVal c.ctr)))
   (let ((?x58566 (c.channel3 ?x71475)))
   (let (($x49145 (= ?x58566 ?x34831)))
   (let (($x33193 (not $x49145)))
   (let (($x73356 (and $x33193 $x11057)))
   (not $x73356))))))))))))))))))
(check-sat)
(pop 0)

(push 2)
  (assert
   (let ((?x1486 (+ 1 en_message)))
   (let (($x19312 (= c.home_current_command ?x1486)))
   (let (($x44417 (not $x19312)))
   (let (($x40119 (< qj1 c.sh_tl)))
   (let (($x65 (not $x40119)))
   (let (($x21952 (= c.sh_hd qj1)))
   (let (($x37693 (< c.sh_hd qj1)))
   (let (($x20865 (or $x37693 $x21952)))
   (let (($x33847 (and $x20865 $x65)))
   (let (($x17495 (not (= (c.channel3 qi1) (+ 1 (+ 1 (+ 1 ?x1486)))))))
   (let (($x15598 (and $x17495 $x33847)))
   (let (($x12114 (not (= (c.channel2_4 qi1) (+ 1 (+ 1 ?x1486))))))
   (let (($x29713 (and $x12114 $x15598)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x60908 (+ 1 ?x34647)))
   (let ((?x83998 (c.channel2_4 qi1)))
   (let (($x63890 (= ?x83998 ?x60908)))
   (let (($x43423 (and $x63890 $x29713)))
   (let (($x63682 (= ?x83998 ?x34647)))
   (let (($x16799 (not $x63682)))
   (let (($x74294 (and $x16799 $x43423)))
   (let ((?x46718 (c.cache qi1)))
   (let (($x83356 (= ?x46718 en_cache_state)))
   (let (($x59259 (and $x83356 $x74294)))
   (let (($x8143 (not (= ?x46718 (+ 1 (+ 1 en_cache_state))))))
   (let (($x59076 (and $x8143 $x59259)))
   (let (($x25631 (and $x59076 $x44417)))
   (not $x25631))))))))))))))))))))))))))))))))
  (assert
   (let ((?x12727 (c.sh_pos c.home_current_client)))
   (let (($x77351 (< ?x12727 c.sh_tl)))
   (let (($x20992 (not $x77351)))
   (not $x20992)))))
(check-sat)
(pop 2)

(push 2)
  (assert
   (let (($x40119 (< qj1 c.sh_tl)))
   (let (($x65 (not $x40119)))
   (let (($x21952 (= c.sh_hd qj1)))
   (let (($x37693 (< c.sh_hd qj1)))
   (let (($x20865 (or $x37693 $x21952)))
   (let (($x33847 (and $x20865 $x65)))
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x28955 (c.channel3 c.home_current_client)))
   (let (($x81758 (not (= ?x28955 ?x34831))))
   (let (($x10014 (and $x81758 $x33847)))
   (let (($x63275 (not (= (c.channel2_4 c.home_current_client) ?x30209))))
   (let (($x63197 (and $x63275 $x10014)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x60908 (+ 1 ?x34647)))
   (let ((?x30972 (c.channel2_4 c.home_current_client)))
   (let (($x50264 (= ?x30972 ?x60908)))
   (let (($x19596 (and $x50264 $x63197)))
   (let (($x31844 (= ?x30972 ?x34647)))
   (let (($x33315 (not $x31844)))
   (let (($x18476 (and $x33315 $x19596)))
   (let ((?x32741 (c.cache c.home_current_client)))
   (let (($x71752 (= ?x32741 en_cache_state)))
   (let (($x2014 (and $x71752 $x18476)))
   (let (($x64615 (not (= ?x32741 (+ 1 (+ 1 en_cache_state))))))
   (let (($x22598 (and $x64615 $x2014)))
   (let (($x32504 (not (c.home_invalidate_list c.home_current_client))))
   (let (($x54895 (and $x32504 $x22598)))
   (let (($x62406 (= c.sh_hd c.sh_tl)))
   (let (($x27620 (not $x62406)))
   (let (($x58255 (and $x27620 $x54895)))
   (let (($x701 (and c.home_exclusive_granted $x58255)))
   (let (($x19312 (= c.home_current_command ?x1486)))
   (let (($x44417 (not $x19312)))
   (let (($x12292 (and $x44417 $x701)))
   (let (($x37805 (= c.home_current_command ?x46960)))
   (let (($x30892 (not $x37805)))
   (let (($x24398 (and $x30892 $x12292)))
   (let ((?x23348 (c.sh_q c.sh_hd)))
   (let (($x57487 (= c.home_current_client ?x23348)))
   (let (($x17522 (and $x57487 $x24398)))
   (let ((?x12727 (c.sh_pos c.home_current_client)))
   (let (($x77351 (< ?x12727 c.sh_tl)))
   (let (($x20992 (not $x77351)))
   (let (($x77120 (= c.sh_hd ?x12727)))
   (let (($x47506 (< c.sh_hd ?x12727)))
   (let (($x30131 (or $x47506 $x77120)))
   (let (($x11057 (and $x30131 $x20992)))
   (let (($x17495 (not (= (c.channel3 qi1) ?x34831))))
   (let (($x41621 (and $x17495 $x11057)))
   (let (($x12114 (not (= (c.channel2_4 qi1) ?x30209))))
   (let (($x33485 (and $x12114 $x41621)))
   (let ((?x83998 (c.channel2_4 qi1)))
   (let (($x63890 (= ?x83998 ?x60908)))
   (let (($x10956 (not $x63890)))
   (let (($x11505 (and $x10956 $x33485)))
   (let (($x63682 (= ?x83998 ?x34647)))
   (let (($x16799 (not $x63682)))
   (let (($x23061 (and $x16799 $x11505)))
   (let ((?x46718 (c.cache qi1)))
   (let (($x83356 (= ?x46718 en_cache_state)))
   (let (($x14021 (and $x83356 $x23061)))
   (let (($x8143 (not (= ?x46718 (+ 1 (+ 1 en_cache_state))))))
   (let (($x51162 (and $x8143 $x14021)))
   (let (($x7005 (c.home_invalidate_list qi1)))
   (let (($x41153 (not $x7005)))
   (let (($x26010 (and $x41153 $x51162)))
   (let (($x1577 (and $x62406 $x26010)))
   (let (($x41063 (and $x1577 $x17522)))
   (not $x41063)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  (assert
   (let ((?x38967 (+ 1 c.sh_tl)))
   (let ((?x12727 (c.sh_pos c.home_current_client)))
   (let ((?x33081 (c.sh_q ?x12727)))
   (let (($x39227 (= ?x33081 c.home_current_client)))
   (let (($x77351 (< ?x12727 c.sh_tl)))
   (let (($x77120 (= c.sh_hd ?x12727)))
   (let (($x47506 (< c.sh_hd ?x12727)))
   (let (($x30131 (or $x47506 $x77120)))
   (let (($x11543 (and $x30131 $x77351)))
   (let (($x23296 (not (and $x11543 $x39227))))
   (let ((?x30972 (c.channel2_4 c.home_current_client)))
   (let (($x11472 (= ?x30972 en_message)))
   (let (($x62406 (= c.sh_hd c.sh_tl)))
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let (($x37805 (= c.home_current_command ?x46960)))
   (let (($x38722 (and $x37805 $x62406)))
   (let (($x49926 (and $x38722 $x11472)))
   (let (($x17040 (and c.x2 c.x3)))
   (let (($x2836 (and $x17040 $x49926)))
   (let (($x22657 (and $x2836 $x23296)))
   (let (($x51903 (and (and (= c.home_current_command ?x1486) (not c.home_exclusive_granted)) $x11472)))
   (let (($x78018 (and (and (not c.x2) c.x3) $x51903)))
   (let (($x32149 (and $x78018 $x23296)))
   (let ((?x77487 (ite $x32149 ?x38967 (ite $x22657 ?x38967 c.sh_tl))))
   (let (($x31589 (< qj1 ?x77487)))
   (let (($x82790 (not $x31589)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x71475 (c.ArbVal c.ctr)))
   (let ((?x58566 (c.channel3 ?x71475)))
   (let (($x49145 (= ?x58566 ?x34831)))
   (let (($x33193 (not $x49145)))
   (let (($x17413 (and $x33193 $x82790)))
   (not $x17413))))))))))))))))))))))))))))))))))))
(check-sat)
(pop 2)

(push 2)
  (assert
   (let ((?x75590 (+ 1 c.sh_hd)))
   (let (($x30269 (< ?x75590 c.sh_tl)))
   (let (($x59696 (not $x30269)))
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x62427 (c.channel3 qi1)))
   (let (($x17495 (not (= ?x62427 ?x34831))))
   (let (($x49587 (and $x17495 $x59696)))
   (let (($x12114 (not (= (c.channel2_4 qi1) ?x30209))))
   (let (($x75364 (and $x12114 $x49587)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x60908 (+ 1 ?x34647)))
   (let ((?x83998 (c.channel2_4 qi1)))
   (let (($x63890 (= ?x83998 ?x60908)))
   (let (($x51249 (and $x63890 $x75364)))
   (let (($x63682 (= ?x83998 ?x34647)))
   (let (($x16799 (not $x63682)))
   (let (($x64373 (and $x16799 $x51249)))
   (let ((?x46718 (c.cache qi1)))
   (let (($x83356 (= ?x46718 en_cache_state)))
   (let (($x24821 (and $x83356 $x64373)))
   (let (($x8143 (not (= ?x46718 (+ 1 (+ 1 en_cache_state))))))
   (let (($x24801 (and $x8143 $x24821)))
   (let (($x7005 (c.home_invalidate_list qi1)))
   (let (($x41153 (not $x7005)))
   (let (($x52058 (and $x41153 $x24801)))
   (let (($x62406 (= c.sh_hd c.sh_tl)))
   (let (($x27620 (not $x62406)))
   (let (($x52761 (and $x27620 $x52058)))
   (and c.home_exclusive_granted $x52761)))))))))))))))))))))))))))))))))
  (assert
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x71475 (c.ArbVal c.ctr)))
   (let ((?x58566 (c.channel3 ?x71475)))
   (let (($x49145 (= ?x58566 ?x34831)))
   (let (($x71758 (= c.home_current_command en_message)))
   (let (($x34407 (not $x71758)))
   (let (($x77361 (and (and (and (and (not c.x0) (not c.x1)) c.x2) (not c.x3)) (and $x34407 $x49145))))
   (let (($x79633 (not $x77361)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x30972 (c.channel2_4 c.home_current_client)))
   (let (($x31844 (= ?x30972 ?x34647)))
   (let (($x33315 (not $x31844)))
   (and $x33315 $x79633)))))))))))))))))
(check-sat)
(pop 0)

(push 2)
  (assert
   (let ((?x75590 (+ 1 c.sh_hd)))
   (let (($x30269 (< ?x75590 c.sh_tl)))
   (let (($x59696 (not $x30269)))
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x71475 (c.ArbVal c.ctr)))
   (let ((?x58566 (c.channel3 ?x71475)))
   (let (($x49145 (= ?x58566 ?x34831)))
   (let (($x33193 (not $x49145)))
   (let (($x52647 (and $x33193 $x59696)))
   (let ((?x13783 (c.channel2_4 ?x71475)))
   (let (($x16165 (= ?x13783 ?x30209)))
   (let (($x14680 (not $x16165)))
   (let (($x45397 (and $x14680 $x52647)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x60908 (+ 1 ?x34647)))
   (let (($x2646 (= ?x13783 ?x60908)))
   (let (($x1508 (not $x2646)))
   (let (($x13871 (and $x1508 $x45397)))
   (let (($x13844 (= ?x13783 ?x34647)))
   (let (($x25985 (not $x13844)))
   (let (($x70601 (and $x25985 $x13871)))
   (let ((?x12944 (c.cache ?x71475)))
   (let (($x13259 (= ?x12944 en_cache_state)))
   (let (($x18029 (and $x13259 $x70601)))
   (let (($x13288 (not (= ?x12944 (+ 1 (+ 1 en_cache_state))))))
   (let (($x31338 (and $x13288 $x18029)))
   (let (($x30561 (not $x31338)))
   (not $x30561))))))))))))))))))))))))))))))))
  (assert
   (let ((?x71475 (c.ArbVal c.ctr)))
   (let ((?x12944 (c.cache ?x71475)))
   (let (($x13259 (= ?x12944 en_cache_state)))
   (let (($x72583 (not $x13259)))
   (not $x72583))))))
(check-sat)
(pop 0)

(push 2)
  (assert
   (let ((?x7929 (c.sh_pos qi1)))
   (let (($x52043 (= qi1 c.home_current_client)))
   (let ((?x12727 (c.sh_pos c.home_current_client)))
   (let ((?x33081 (c.sh_q ?x12727)))
   (let (($x39227 (= ?x33081 c.home_current_client)))
   (let (($x77351 (< ?x12727 c.sh_tl)))
   (let (($x77120 (= c.sh_hd ?x12727)))
   (let (($x47506 (< c.sh_hd ?x12727)))
   (let (($x30131 (or $x47506 $x77120)))
   (let (($x11543 (and $x30131 $x77351)))
   (let (($x23296 (not (and $x11543 $x39227))))
   (let ((?x30972 (c.channel2_4 c.home_current_client)))
   (let (($x11472 (= ?x30972 en_message)))
   (let (($x62406 (= c.sh_hd c.sh_tl)))
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let (($x37805 (= c.home_current_command ?x46960)))
   (let (($x38722 (and $x37805 $x62406)))
   (let (($x49926 (and $x38722 $x11472)))
   (let (($x17040 (and c.x2 c.x3)))
   (let (($x2836 (and $x17040 $x49926)))
   (let (($x22657 (and $x2836 $x23296)))
   (let (($x51903 (and (and (= c.home_current_command ?x1486) (not c.home_exclusive_granted)) $x11472)))
   (let (($x78018 (and (and (not c.x2) c.x3) $x51903)))
   (let (($x32149 (and $x78018 $x23296)))
   (let ((?x71475 (c.ArbVal c.ctr)))
   (let ((?x9577 (c.sh_pos ?x71475)))
   (let (($x7942 (< ?x9577 c.sh_tl)))
   (let (($x41171 (= c.sh_hd ?x9577)))
   (let (($x77764 (< c.sh_hd ?x9577)))
   (let (($x36355 (or $x77764 $x41171)))
   (let (($x15931 (= qi1 ?x71475)))
   (let (($x20041 (not $x15931)))
   (let ((?x23348 (c.sh_q c.sh_hd)))
   (let (($x38442 (= qi1 ?x23348)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x58566 (c.channel3 ?x71475)))
   (let (($x49145 (= ?x58566 ?x34831)))
   (let (($x71758 (= c.home_current_command en_message)))
   (let (($x34407 (not $x71758)))
   (let (($x77361 (and (and (and (and (not c.x0) (not c.x1)) c.x2) (not c.x3)) (and $x34407 $x49145))))
   (let ((?x31267 (ite (and (and (and (and $x77361 $x38442) $x20041) $x36355) $x7942) ?x9577 (ite (and $x32149 $x52043) c.sh_tl (ite (and $x22657 $x52043) c.sh_tl ?x7929)))))
   (let (($x30709 (= qj1 (ite (and (and (and $x77361 $x15931) $x36355) $x7942) c.sh_hd ?x31267))))
   (let (($x36650 (not $x30709)))
   (let (($x25069 (and $x36355 $x7942)))
   (let (($x33193 (not $x49145)))
   (let (($x60324 (and $x33193 $x25069)))
   (let ((?x13783 (c.channel2_4 ?x71475)))
   (let (($x16165 (= ?x13783 ?x30209)))
   (let (($x14680 (not $x16165)))
   (let (($x30683 (and $x14680 $x60324)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x60908 (+ 1 ?x34647)))
   (let (($x2646 (= ?x13783 ?x60908)))
   (let (($x1508 (not $x2646)))
   (let (($x47693 (and $x1508 $x30683)))
   (let (($x27837 (not $x47693)))
   (and $x27837 $x36650))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  (assert
   (let ((?x71475 (c.ArbVal c.ctr)))
   (let (($x74119 (c.home_invalidate_list ?x71475)))
   (not $x74119))))
(check-sat)
(pop 0)

(push 2)
  (assert
   (let ((?x71475 (c.ArbVal c.ctr)))
   (let ((?x9577 (c.sh_pos ?x71475)))
   (let (($x7942 (< ?x9577 c.sh_tl)))
   (let (($x2377 (not $x7942)))
   (let (($x41171 (= c.sh_hd ?x9577)))
   (let (($x77764 (< c.sh_hd ?x9577)))
   (let (($x36355 (or $x77764 $x41171)))
   (let (($x39464 (and $x36355 $x2377)))
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x58566 (c.channel3 ?x71475)))
   (let (($x49145 (= ?x58566 ?x34831)))
   (let (($x33193 (not $x49145)))
   (let (($x20136 (and $x33193 $x39464)))
   (let ((?x13783 (c.channel2_4 ?x71475)))
   (let (($x16165 (= ?x13783 ?x30209)))
   (let (($x14680 (not $x16165)))
   (let (($x65242 (and $x14680 $x20136)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x60908 (+ 1 ?x34647)))
   (let (($x2646 (= ?x13783 ?x60908)))
   (let (($x1508 (not $x2646)))
   (let (($x63745 (and $x1508 $x65242)))
   (let (($x13844 (= ?x13783 ?x34647)))
   (let (($x25985 (not $x13844)))
   (let (($x67525 (and $x25985 $x63745)))
   (let ((?x12944 (c.cache ?x71475)))
   (let (($x13259 (= ?x12944 en_cache_state)))
   (let (($x5709 (and $x13259 $x67525)))
   (let (($x54223 (not $x5709)))
   (not $x54223))))))))))))))))))))))))))))))))))
  (assert
   (let (($x40119 (< qj1 c.sh_tl)))
   (let (($x65 (not $x40119)))
   (let (($x21952 (= c.sh_hd qj1)))
   (let (($x37693 (< c.sh_hd qj1)))
   (let (($x20865 (or $x37693 $x21952)))
   (let (($x33847 (and $x20865 $x65)))
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x71475 (c.ArbVal c.ctr)))
   (let ((?x58566 (c.channel3 ?x71475)))
   (let (($x49145 (= ?x58566 ?x34831)))
   (let (($x33193 (not $x49145)))
   (let (($x18085 (and $x33193 $x33847)))
   (let ((?x13783 (c.channel2_4 ?x71475)))
   (let (($x16165 (= ?x13783 ?x30209)))
   (let (($x14680 (not $x16165)))
   (let (($x13987 (and $x14680 $x18085)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x60908 (+ 1 ?x34647)))
   (let (($x2646 (= ?x13783 ?x60908)))
   (let (($x1508 (not $x2646)))
   (let (($x39728 (and $x1508 $x13987)))
   (let (($x13844 (= ?x13783 ?x34647)))
   (let (($x17321 (and $x13844 $x39728)))
   (not $x17321))))))))))))))))))))))))))))
(check-sat)
(pop 1)

(push 2)
  (assert
   (let (($x2950 (< c.sh_hd c.sh_tl)))
   (let (($x44063 (not $x2950)))
   (not $x44063))))
  (assert
   (let (($x12114 (not (= (c.channel2_4 qi1) (+ 1 (+ 1 (+ 1 en_message)))))))
   (let (($x24733 (not $x12114)))
   (not $x24733))))
(check-sat)
(pop 1)

(push 2)
  (assert
   (let ((?x75590 (+ 1 c.sh_hd)))
   (let (($x30269 (< ?x75590 c.sh_tl)))
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x62427 (c.channel3 qi1)))
   (let (($x17495 (not (= ?x62427 ?x34831))))
   (let (($x69911 (and $x17495 $x30269)))
   (let (($x12114 (not (= (c.channel2_4 qi1) ?x30209))))
   (let (($x15613 (and $x12114 $x69911)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x60908 (+ 1 ?x34647)))
   (let ((?x83998 (c.channel2_4 qi1)))
   (let (($x63890 (= ?x83998 ?x60908)))
   (let (($x10956 (not $x63890)))
   (let (($x51693 (and $x10956 $x15613)))
   (let (($x63682 (= ?x83998 ?x34647)))
   (let (($x55123 (and $x63682 $x51693)))
   (let ((?x46718 (c.cache qi1)))
   (let (($x83356 (= ?x46718 en_cache_state)))
   (let (($x39765 (and $x83356 $x55123)))
   (let (($x8143 (not (= ?x46718 (+ 1 (+ 1 en_cache_state))))))
   (let (($x23443 (and $x8143 $x39765)))
   (let (($x7005 (c.home_invalidate_list qi1)))
   (let (($x41153 (not $x7005)))
   (let (($x73786 (and $x41153 $x23443)))
   (let (($x62406 (= c.sh_hd c.sh_tl)))
   (let (($x27620 (not $x62406)))
   (let (($x45833 (and $x27620 $x73786)))
   (not $x45833))))))))))))))))))))))))))))))))
  (assert
   (let (($x2950 (< c.sh_hd c.sh_tl)))
   (let (($x44063 (not $x2950)))
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x71475 (c.ArbVal c.ctr)))
   (let ((?x58566 (c.channel3 ?x71475)))
   (let (($x49145 (= ?x58566 ?x34831)))
   (let (($x33193 (not $x49145)))
   (let (($x57255 (and $x33193 $x44063)))
   (let ((?x13783 (c.channel2_4 ?x71475)))
   (let (($x16165 (= ?x13783 ?x30209)))
   (let (($x14680 (not $x16165)))
   (let (($x34616 (and $x14680 $x57255)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x60908 (+ 1 ?x34647)))
   (let (($x2646 (= ?x13783 ?x60908)))
   (let (($x1508 (not $x2646)))
   (let (($x54061 (and $x1508 $x34616)))
   (let (($x13844 (= ?x13783 ?x34647)))
   (let (($x29396 (and $x13844 $x54061)))
   (let ((?x12944 (c.cache ?x71475)))
   (let (($x13259 (= ?x12944 en_cache_state)))
   (let (($x72093 (and $x13259 $x29396)))
   (let ((?x7929 (c.sh_pos qi1)))
   (let (($x9725 (= c.sh_hd ?x7929)))
   (let (($x349 (not $x9725)))
   (let (($x57867 (and $x349 $x72093)))
   (not $x57867)))))))))))))))))))))))))))))))
(check-sat)
(pop 2)

(push 2)
  (assert
   (let ((?x12727 (c.sh_pos c.home_current_client)))
   (let (($x77351 (< ?x12727 c.sh_tl)))
   (let (($x20992 (not $x77351)))
   (let (($x77120 (= c.sh_hd ?x12727)))
   (let (($x47506 (< c.sh_hd ?x12727)))
   (let (($x30131 (or $x47506 $x77120)))
   (let (($x11057 (and $x30131 $x20992)))
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x62427 (c.channel3 qi1)))
   (let (($x17495 (not (= ?x62427 ?x34831))))
   (let (($x41621 (and $x17495 $x11057)))
   (let (($x12114 (not (= (c.channel2_4 qi1) ?x30209))))
   (let (($x33485 (and $x12114 $x41621)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x60908 (+ 1 ?x34647)))
   (let ((?x83998 (c.channel2_4 qi1)))
   (let (($x63890 (= ?x83998 ?x60908)))
   (let (($x9518 (and $x63890 $x33485)))
   (let (($x63682 (= ?x83998 ?x34647)))
   (let (($x16799 (not $x63682)))
   (let (($x45824 (and $x16799 $x9518)))
   (let ((?x46718 (c.cache qi1)))
   (let (($x83356 (= ?x46718 en_cache_state)))
   (let (($x48027 (and $x83356 $x45824)))
   (let (($x8143 (not (= ?x46718 (+ 1 (+ 1 en_cache_state))))))
   (let (($x70799 (and $x8143 $x48027)))
   (let (($x7005 (c.home_invalidate_list qi1)))
   (let (($x41153 (not $x7005)))
   (let (($x70683 (and $x41153 $x70799)))
   (let (($x62406 (= c.sh_hd c.sh_tl)))
   (let (($x27620 (not $x62406)))
   (let (($x70861 (and $x27620 $x70683)))
   (let (($x35461 (and c.home_exclusive_granted $x70861)))
   (let (($x19312 (= c.home_current_command ?x1486)))
   (let (($x44417 (not $x19312)))
   (let (($x52935 (and $x44417 $x35461)))
   (let (($x37805 (= c.home_current_command ?x46960)))
   (let (($x30892 (not $x37805)))
   (let (($x71001 (and $x30892 $x52935)))
   (not $x71001))))))))))))))))))))))))))))))))))))))))))))
  (assert
   (let ((?x12727 (c.sh_pos c.home_current_client)))
   (let (($x77351 (< ?x12727 c.sh_tl)))
   (let (($x20992 (not $x77351)))
   (let (($x77120 (= c.sh_hd ?x12727)))
   (let (($x47506 (< c.sh_hd ?x12727)))
   (let (($x30131 (or $x47506 $x77120)))
   (let (($x11057 (and $x30131 $x20992)))
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x62427 (c.channel3 qi1)))
   (let (($x17495 (not (= ?x62427 ?x34831))))
   (let (($x41621 (and $x17495 $x11057)))
   (let (($x12114 (not (= (c.channel2_4 qi1) ?x30209))))
   (let (($x33485 (and $x12114 $x41621)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x60908 (+ 1 ?x34647)))
   (let ((?x83998 (c.channel2_4 qi1)))
   (let (($x63890 (= ?x83998 ?x60908)))
   (let (($x10956 (not $x63890)))
   (let (($x11505 (and $x10956 $x33485)))
   (let (($x63682 (= ?x83998 ?x34647)))
   (let (($x16799 (not $x63682)))
   (let (($x23061 (and $x16799 $x11505)))
   (let ((?x46718 (c.cache qi1)))
   (let (($x83356 (= ?x46718 en_cache_state)))
   (let (($x14021 (and $x83356 $x23061)))
   (let (($x8143 (not (= ?x46718 (+ 1 (+ 1 en_cache_state))))))
   (let (($x51162 (and $x8143 $x14021)))
   (not $x51162))))))))))))))))))))))))))))))))
(check-sat)
(pop 0)

(push 2)
  (assert
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x83998 (c.channel2_4 qi1)))
   (let (($x63682 (= ?x83998 ?x34647)))
   (let (($x16799 (not $x63682)))
   (let (($x17495 (not (= (c.channel3 qi1) ?x34831))))
   (and $x17495 $x16799)))))))))))
  (assert
   (let (($x2950 (< c.sh_hd c.sh_tl)))
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x62427 (c.channel3 qi1)))
   (let (($x17495 (not (= ?x62427 ?x34831))))
   (let (($x359 (and $x17495 $x2950)))
   (let (($x12114 (not (= (c.channel2_4 qi1) ?x30209))))
   (let (($x20502 (and $x12114 $x359)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x60908 (+ 1 ?x34647)))
   (let ((?x83998 (c.channel2_4 qi1)))
   (let (($x63890 (= ?x83998 ?x60908)))
   (let (($x10956 (not $x63890)))
   (let (($x46015 (and $x10956 $x20502)))
   (let (($x63682 (= ?x83998 ?x34647)))
   (let (($x73761 (and $x63682 $x46015)))
   (let ((?x46718 (c.cache qi1)))
   (let (($x83356 (= ?x46718 en_cache_state)))
   (let (($x56358 (and $x83356 $x73761)))
   (let (($x8143 (not (= ?x46718 (+ 1 (+ 1 en_cache_state))))))
   (let (($x62317 (and $x8143 $x56358)))
   (let ((?x71475 (c.ArbVal c.ctr)))
   (let ((?x9577 (c.sh_pos ?x71475)))
   (let (($x7942 (< ?x9577 c.sh_tl)))
   (let (($x41171 (= c.sh_hd ?x9577)))
   (let (($x77764 (< c.sh_hd ?x9577)))
   (let (($x36355 (or $x77764 $x41171)))
   (let (($x25069 (and $x36355 $x7942)))
   (let (($x73682 (and $x17495 $x25069)))
   (let (($x20276 (and $x12114 $x73682)))
   (let (($x24539 (and $x63890 $x20276)))
   (let (($x16799 (not $x63682)))
   (let (($x26947 (and $x16799 $x24539)))
   (let (($x3781 (and $x83356 $x26947)))
   (let (($x46890 (and $x8143 $x3781)))
   (let (($x7005 (c.home_invalidate_list qi1)))
   (let (($x41153 (not $x7005)))
   (let (($x49521 (and $x41153 $x46890)))
   (let (($x62406 (= c.sh_hd c.sh_tl)))
   (let (($x27620 (not $x62406)))
   (let (($x62390 (and $x27620 $x49521)))
   (let (($x7790 (and c.home_exclusive_granted $x62390)))
   (let (($x19312 (= c.home_current_command ?x1486)))
   (let (($x44417 (not $x19312)))
   (let (($x2365 (and $x44417 $x7790)))
   (let (($x37805 (= c.home_current_command ?x46960)))
   (let (($x30892 (not $x37805)))
   (let (($x46072 (and $x30892 $x2365)))
   (let ((?x23348 (c.sh_q c.sh_hd)))
   (let (($x38442 (= qi1 ?x23348)))
   (let (($x42859 (and $x38442 $x46072)))
   (let ((?x3281 (c.sh_q ?x9577)))
   (let (($x53512 (= qi1 ?x3281)))
   (let (($x64835 (and $x53512 $x42859)))
   (let (($x24086 (and $x64835 $x62317)))
   (not $x24086)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(pop 0)

(push 2)
  (assert
   (let ((?x71475 (c.ArbVal c.ctr)))
   (let ((?x9577 (c.sh_pos ?x71475)))
   (let (($x7942 (< ?x9577 c.sh_tl)))
   (let (($x2377 (not $x7942)))
   (let (($x41171 (= c.sh_hd ?x9577)))
   (let (($x77764 (< c.sh_hd ?x9577)))
   (let (($x36355 (or $x77764 $x41171)))
   (let (($x39464 (and $x36355 $x2377)))
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x58566 (c.channel3 ?x71475)))
   (let (($x49145 (= ?x58566 ?x34831)))
   (let (($x33193 (not $x49145)))
   (let (($x20136 (and $x33193 $x39464)))
   (let ((?x13783 (c.channel2_4 ?x71475)))
   (let (($x16165 (= ?x13783 ?x30209)))
   (let (($x14680 (not $x16165)))
   (let (($x65242 (and $x14680 $x20136)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x60908 (+ 1 ?x34647)))
   (let (($x2646 (= ?x13783 ?x60908)))
   (let (($x1508 (not $x2646)))
   (let (($x63745 (and $x1508 $x65242)))
   (let (($x13844 (= ?x13783 ?x34647)))
   (let (($x25985 (not $x13844)))
   (let (($x67525 (and $x25985 $x63745)))
   (let ((?x12944 (c.cache ?x71475)))
   (let (($x13259 (= ?x12944 en_cache_state)))
   (let (($x5709 (and $x13259 $x67525)))
   (let (($x13288 (not (= ?x12944 (+ 1 (+ 1 en_cache_state))))))
   (let (($x50728 (and $x13288 $x5709)))
   (let (($x74119 (c.home_invalidate_list ?x71475)))
   (let (($x77139 (not $x74119)))
   (let (($x70996 (and $x77139 $x50728)))
   (let (($x62406 (= c.sh_hd c.sh_tl)))
   (let (($x69483 (and $x62406 $x70996)))
   (let (($x9751 (not c.home_exclusive_granted)))
   (let (($x74699 (and $x9751 $x69483)))
   (let ((?x12727 (c.sh_pos c.home_current_client)))
   (let (($x77120 (= c.sh_hd ?x12727)))
   (let (($x47506 (< c.sh_hd ?x12727)))
   (let (($x30131 (or $x47506 $x77120)))
   (let (($x67392 (not $x30131)))
   (let (($x37686 (and $x67392 $x74699)))
   (not $x37686))))))))))))))))))))))))))))))))))))))))))))))))
  (assert
   (let ((?x71475 (c.ArbVal c.ctr)))
   (let ((?x9577 (c.sh_pos ?x71475)))
   (let (($x7942 (< ?x9577 c.sh_tl)))
   (let (($x41171 (= c.sh_hd ?x9577)))
   (let (($x77764 (< c.sh_hd ?x9577)))
   (let (($x36355 (or $x77764 $x41171)))
   (let (($x54592 (not $x36355)))
   (let (($x5247 (and $x54592 $x7942)))
   (not $x5247))))))))))
(check-sat)
(pop 0)

(push 2)
  (assert
   (let ((?x75590 (+ 1 c.sh_hd)))
   (let (($x30269 (< ?x75590 c.sh_tl)))
   (let (($x59696 (not $x30269)))
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x62427 (c.channel3 qi1)))
   (let (($x17495 (not (= ?x62427 ?x34831))))
   (let (($x49587 (and $x17495 $x59696)))
   (let (($x12114 (not (= (c.channel2_4 qi1) ?x30209))))
   (let (($x75364 (and $x12114 $x49587)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x60908 (+ 1 ?x34647)))
   (let ((?x83998 (c.channel2_4 qi1)))
   (let (($x63890 (= ?x83998 ?x60908)))
   (let (($x10956 (not $x63890)))
   (let (($x34907 (and $x10956 $x75364)))
   (let (($x63682 (= ?x83998 ?x34647)))
   (let (($x70402 (and $x63682 $x34907)))
   (let ((?x46718 (c.cache qi1)))
   (let (($x83356 (= ?x46718 en_cache_state)))
   (let (($x2855 (and $x83356 $x70402)))
   (let (($x8143 (not (= ?x46718 (+ 1 (+ 1 en_cache_state))))))
   (let (($x75550 (and $x8143 $x2855)))
   (let (($x7005 (c.home_invalidate_list qi1)))
   (let (($x41153 (not $x7005)))
   (let (($x75987 (and $x41153 $x75550)))
   (not $x75987))))))))))))))))))))))))))))))
  (assert
   (let ((?x1486 (+ 1 en_message)))
   (let ((?x46960 (+ 1 ?x1486)))
   (let ((?x30209 (+ 1 ?x46960)))
   (let ((?x34831 (+ 1 ?x30209)))
   (let ((?x34647 (+ 1 ?x34831)))
   (let ((?x30972 (c.channel2_4 c.home_current_client)))
   (let (($x31844 (= ?x30972 ?x34647)))
   (let (($x33315 (not $x31844)))
   (let (($x32771 (not $x33315)))
   (not $x32771)))))))))))
(check-sat)
(pop 2)

(push 2)
  (assert
   (let ((?x71475 (c.ArbVal c.ctr)))
   (let ((?x9577 (c.sh_pos ?x71475)))
   (let (($x41171 (= c.sh_hd ?x9577)))
   (let (($x13288 (not (= (c.cache ?x71475) (+ 1 (+ 1 en_cache_state))))))
   (let (($x4131 (and $x13288 $x41171)))
   (not $x4131)))))))
  (assert
   (let ((?x23348 (c.sh_q c.sh_hd)))
   (let (($x38442 (= qi1 ?x23348)))
   (let (($x56638 (not $x38442)))
   (not $x56638)))))
(check-sat)
